package org.sat4j;

import org.sat4j.minisat.SolverFactory;
import org.sat4j.reader.GroupedCNFReader;
import org.sat4j.reader.LecteurDimacs;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;
import org.sat4j.tools.xplain.Explainer;
import org.sat4j.tools.xplain.HighLevelXplain;
import org.sat4j.tools.xplain.MinimizationStrategy;
import org.sat4j.tools.xplain.Xplain;

public class MUSLauncher extends AbstractLauncher
{

	public MUSLauncher()
	{
		highLevel = false;
	}

	public void usage()
	{
		log("java -jar sat4j-mus.jar [Insertion|Deletion|QuickXplain] <cnffile>|<gcnffile>");
	}

	@SuppressWarnings("unchecked")
	protected Reader createReader(ISolver isolver, String s)
	{
		if (highLevel)
			return new GroupedCNFReader((HighLevelXplain<ISolver>) isolver);
		else
			return new LecteurDimacs(isolver);
	}

	protected String getInstanceName(String as[])
	{
		if (as.length == 0)
			return null;
		else
			return as[as.length - 1];
	}

	protected ISolver configureSolver(String as[])
	{
		String s = as[as.length - 1];
		if (s.endsWith(".gcnf"))
		{
			highLevel = true;
		}
		Object obj;
		if (highLevel)
		{
			HighLevelXplain<ISolver> highlevelxplain = new HighLevelXplain<ISolver>(
					SolverFactory.newDefault());
			xplain = highlevelxplain;
			obj = highlevelxplain;
		}
		else
		{
			Xplain<ISolver> xplain1 = new Xplain<ISolver>(
					SolverFactory.newDefault());
			xplain = xplain1;
			obj = xplain1;
		}
		if (as.length == 2)
		{
			String s1 = "org.sat4j.tools.xplain." + as[0] + "Strategy";
			try
			{
				xplain.setMinimizationStrategy((MinimizationStrategy) Class
						.forName(s1).newInstance());
			}
			catch (Exception exception)
			{
				log(exception.getMessage());
			}
		}
		((ISolver) (obj)).setTimeout(2147483647);
		((ISolver) (obj)).setDBSimplificationAllowed(true);
		getLogWriter().println(((ISolver) (obj)).toString("c "));
		return ((ISolver) (obj));
	}

	protected void displayResult()
	{
		if (solver != null)
		{
			double d = (double) (System.currentTimeMillis() - beginTime) / 1000D;
			solver.printStat(out, "c ");
			solver.printInfos(out, "c ");
			out.println("s " + exitCode);
			if (exitCode == ExitCode.SATISFIABLE)
			{
				int ai[] = solver.model();
				out.print("v ");
				reader.decode(ai, out);
				out.println();
			}
			else if (exitCode == ExitCode.UNSATISFIABLE && mus != null)
			{
				out.print("v ");
				reader.decode(mus, out);
				out.println();
			}
			log("Total wall clock time (in seconds) : " + d);
		}
	}

	public void run(String as[])
	{
		mus = null;
		super.run(as);
		double d = (double) (System.currentTimeMillis() - beginTime) / 1000D;
		if (exitCode == ExitCode.UNSATISFIABLE)
			try
			{
				log("Unsat detection wall clock time (in seconds) : " + d);
				log("Size of initial " + (highLevel ? "high level " : "")
						+ "unsat subformula: "
						+ solver.unsatExplanation().size());
				log("Computing " + (highLevel ? "high level " : "") + "MUS ...");
				double d1 = System.currentTimeMillis();
				mus = xplain.minimalExplanation();
				log("Size of the " + (highLevel ? "high level " : "") + "MUS: "
						+ mus.length);
				log("Unsat core  computation wall clock time (in seconds) : "
						+ ((double) System.currentTimeMillis() - d1) / 1000D);
			}
			catch (TimeoutException _ex)
			{
				log("Cannot compute " + (highLevel ? "high level " : "")
						+ "MUS within the timeout.");
			}
	}

	public static void main(String args[])
	{
		MUSLauncher muslauncher = new MUSLauncher();
		if (args.length < 1 || args.length > 2)
		{
			muslauncher.usage();
			return;
		}
		else
		{
			muslauncher.run(args);
			System.exit(muslauncher.getExitCode().value());
			return;
		}
	}

	private static final long serialVersionUID = 1L;
	private int mus[];
	private Explainer xplain;
	private boolean highLevel;
}
